import atom.UnaryAtom;
import formula.BinaryFormula;
import formula.Formula;
import formula.UnaryFormula;
import literal.UnaryLiteral;
import proof.ConclusionProof;
import proof.Proof;
import sign.FormulaSign;

import java.util.ArrayList;

public class test_negated {
    public static void main(String[] args) {
        UnaryFormula q = new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"), false));
        UnaryFormula l = new UnaryFormula(new UnaryLiteral(new UnaryAtom("l"), false));

        UnaryFormula p = new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"), false));
        UnaryFormula not_p = new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"), true));
        UnaryFormula not_q = new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"), true));

        boolean flag;
        flag = q.isNegated(l);
        System.out.println(flag);//false

        flag = p.isNegated(not_p);
        System.out.println(flag);//true

        BinaryFormula f1 = new BinaryFormula(FormulaSign.ANY, q, l);//ANY(q,l)

        BinaryFormula negated_f1 = f1.getNegated();
        System.out.println(negated_f1.toString());//Exist(q,not l)

        BinaryFormula f2 = new BinaryFormula(FormulaSign.EXIST, p, q);//Exist(p,q)
        System.out.println(f2.getNegated().toString());//ANY(p,not q)
        //System.out.println(f2.isNegated(f2.getNegated()));

        BinaryFormula f3 = new BinaryFormula(FormulaSign.EXIST, p, not_q);//Exist(p,not q)
        System.out.println(f3.getNegated().toString());//ANY(p,q)


        //对UnaryAtom进行取反的测试
//        UnaryFormula unaryformula=q.getNegated();
//        System.out.println(unaryformula.toString());//not q
//
//        unaryformula=not_q.getNegated();
//        System.out.println(unaryformula);




    }
}
